Computer and Modernization ›› 2010, Vol. 1 ›› Issue (8): 58-61.doi: 10.3969/j.issn.1006-2475.2010.08.017

• 人工智能 • Previous Articles     Next Articles

A Method for Linear Temporal Logic Programs Model Checking Based on Büchi Automaton

LUO Qing-sheng   

  1. International School of Jiangxi University of Finance & Economics, Nanchang 330013, China
  • Received:2010-04-09 Revised:1900-01-01 Online:2010-08-27 Published:2010-08-27

Abstract: Formal verification of temporal logic programs plays an important role in improving program correctness. Corresponding Büchi Automaton is constructed based on automata theory, in which labeled transition system（S） indicating programs’ acts, temporal logic formulas（F） indicating programs’ property. Thus, it proves that whether formal formula S |=F is satisfiable or not.

Key words: Linear time temporal logic, Büchi automaton, model checking